COMMENT ⊗   VALID 00013 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	This is the execise file for the FOL primer, AIM-288.  Through page twelve
C00004 00003	> new FOL core image >
C00005 00004	> new FOL core image >
C00007 00005	> new FOL core image >
C00009 00006	> this won't work unless you make the appropriate declarations >
C00010 00007	> new FOL core image >
C00012 00008	DECLARE PREDCONST ALLTHESAME (GRID)[PRE]
C00013 00009	ASSUME  ALLTHESAME G∧COLOROF(G,S21)=RED
C00014 00010	REPRESENT * AS UNIVERSE
C00017 00011	FUNCTION (DE NEXT (S L)
C00019 00012	> the show commands >
C00020 00013	Deduce the WFF
C00021 ENDMK
C⊗;
This is the execise file for the FOL primer, AIM-288.  Through page twelve
are the various sample commands given in the primer.  The rest
of this file are exercises for the novice FOL user.  The exercises contain
a difficulty rating (0 to 50) to guide their usage.

If the sample commands are to read in correctly, it is necessary to run FOL
again from the monitor level when the line 
		comment > new FOL core image >
is reached.
comment > new FOL core image >
DECLARE INDCONST Socrates;
DECLARE PREDCONST MORTAL MAN 1;
DECLARE INDVAR x;
ASSUME MAN(Socrates)∧∀x.(MAN(x)⊃MORTAL(x));
TAUT ∀x.(MAN(x)⊃MORTAL(x)) 1;
∀E 2 Socrates;
TAUT MORTAL(Socrates) 1,3;
⊃I 1⊃4;
comment > new FOL core image >
DECLARE INDCONST ONE, TWO, THREE, BB, WW, BW, BLACKS, WHITES;
DECLARE PREDCONST BOX 1;
DECLARE PREDCONST IS LABELED HAS 2;
DECLARE INDVAR x,y,z;
AXIOM  AREBOX:
       ∀x.(BOX(x) ≡ (x=ONE ∨ x=TWO ∨ x=THREE));;
AXIOM LABEL:
	∀ x. (IS(x,BB) ≡ (HAS(x,BLACKS)∧¬HAS(x,WHITES))),
	∀ x. (IS(x,WW) ≡ (HAS(x,WHITES)∧¬HAS(x,BLACKS))),
	∀ x. (IS(x,BW) ≡ (HAS(x,WHITES)∧ HAS(x,BLACKS)));;
AXIOM WRONG_LABEL:
	∀ x y. (LABELED(x,y)⊃¬IS(x,y));;
AXIOM IS_EACH:
	∃ x.  (BOX(x) ∧ IS(x,BB)),
	∃ x.  (BOX(x) ∧ IS(x,WW)),
	∃ x.  (BOX(x) ∧ IS(x,BW));;
∀E WRONG_LABEL ONE BB;
∀E WRONG_LABEL TWO WW;
∀E WRONG_LABEL THREE BW;
∀E LABEL1 ONE;
∀E LABEL2 TWO;
∀E LABEL3 THREE;
∃E IS_EACH1 x;
∃E IS_EACH2 y;
∃E IS_EACH3 z;
∀E AREBOX x;
∀E AREBOX y;
∀E AREBOX z;
TAUTEQ 
	(LABELED(ONE BB)∧LABELED(TWO WW)∧LABELED(THREE BW))⊃(
	(HAS(THREE BLACKS)⊃
		(IS(THREE BB)∧IS(ONE WW)∧IS(TWO BW))) ∧
	(HAS(THREE WHITES)⊃
		(IS(THREE WW)∧IS(ONE BW)∧IS(TWO BB)))) 1:12;
comment > new FOL core image >
DECLARE INDCONST KingofSpades QueenofHearts JackofDiamonds;
DECLARE PREDCONST PLAYINGCARD BLACKCARD 1;
DECLARE INDCONST NineofSpades ε PLAYINGCARD;
DECLARE PREDCONST REDCARD 1;
MOREGENERAL PLAYINGCARD≥{REDCARD};
DECLARE PREDCONST SPADE 1 [PRE];
ASSUME SPADE NineofSpades;
DECLARE PREDCONST SAMESUIT 2;
DECLARE PREDCONST < 2 [INF];
DECLARE PREDCONST JACK,TEN,NINE 1 [PRE];
DECLARE PREDCONST ROYALFLUSH 5;
DECLARE PREDCONST CAPTURES 2;
DECLARE PREDCONST ≤ (NATNUM,NATNUM) [INF];
DECLARE OPCONST SIN COS 1;
DECLARE OPCONST CONS(SEXPR,SEXPR);
DECLARE OPCONST +(NATNUM,NATNUM)=NATNUM [INF];
DECLARE OPCONST PIECEON(BOARD,SQUARE)=CHESSPIECE;
DECLARE INDVAR x,y,z;
DECLARE INDVAR day date month ε TIME;
DECLARE INDVAR C1 C2 C3 ε PLAYINGCARDS;
comment > this won't work unless you make the appropriate declarations >
AXIOM ACES:
      ∀x y.((ACE(x)∧¬ACE(y))⊃CAPTURES(x y)),
      ∀s.(ISSUIT(s)⊃∃x.(ACE(x)∧SUIT(x)=s)),
      SUIT(AceofSpades)=Spade,
      ∀x.(ISACE(x)≡RANK(x)=Ace) ;;
AXIOM ZEROADD: ∀x.(x+0=x);;
comment > new FOL core image >
DECLARE PREDCONST COLOR SQUARE GRID 1[PRE];
DECLARE INDCONST RED GREEN YELLOW BLUEεCOLOR;
DECLARE INDCONST S11 S12 S21 S22 ε SQUARE;
DECLARE OPCONST COLOROF(GRID SQUARE)=COLOR;
DECLARE OPCONST → (SQUARE)=SQUARE;
DECLARE INDVAR G G1 G2 ε GRID;
DECLARE INDVAR S S1 S2 ε SQUARE;
DECLARE INDVAR C C1 C2 CA CB ε COLOR;
DECLARE OPCONST MAKEGRID(COLOR,COLOR,COLOR,COLOR)=GRID;

AXIOM EXTCOLOR:∀C.(C=RED∨C=GREEN∨C=YELLOW∨C=BLUE),
			  ¬RED=GREEN,
			  ¬RED=YELLOW,
			  ¬RED=BLUE,
			  ¬GREEN=YELLOW,
			  ¬GREEN=BLUE,
			  ¬YELLOW=BLUE;;
AXIOM EXTSQUARE:∀S.(S=S11∨S=S12∨S=S21∨S=S22),
			  ¬S11=S12,
			  ¬S11=S21,
			  ¬S11=S22,
			  ¬S12=S21,
			  ¬S12=S22,
			  ¬S21=S22;;
AXIOM GRIDSIZE:
	 ∀G.(G=MAKEGRID(COLOROF(G S11)
		        COLOROF(G S12),
			COLOROF(G S21),
			COLOROF(G S22)));;
AXIOM NEXTSQUARE:  →(S11)=S12,
			   →(S12)=S22,
			   →(S22)=S21,
			   →(S21)=S11;;
DECLARE PREDCONST ALLTHESAME (GRID)[PRE];
DECLARE PREDCONST ALLDIFFERENT(GRID)[PRE];
DECLARE PREDCONST HAS(GRID COLOR);
DECLARE PREDCONST PLAID(GRID)[PRE];
DECLARE PREDCONST FREEOF(GRID COLOR);
AXIOM DEFINITIONS:
	     ∀G.(ALLTHESAME G≡∃C.∀S.COLOROF(G S)=C),
	     ∀G.(ALLDIFFERENT G≡
		    ∀S1 S2.(COLOROF(G S1)=COLOROF(G S2)⊃S1=S2)),
	     ∀G C.(HAS(G C)≡∃S.COLOROF(G S)=C),
	     ∀G.(PLAID G≡∀S1.∃C1 C2.(¬C1=C2∧(COLOROF(G S1)=C1∧
					 COLOROF(G →(S1))=C2∧
					 COLOROF(G →(→(S1)))=C1))),
	     ∀G C.(FREEOF(G C)≡∀S.¬COLOROF(G S)=C);;
ASSUME  ALLTHESAME G∧COLOROF(G,S21)=RED;
∀E DEFINITIONS1 G ;
TAUT ∃C.∀S.COLOROF(G,S)=C 1,2;
∃E 3 C;
∀E 4 S21 ;
∀E 4 S;
TAUTEQ ¬COLOROF(G,S)=GREEN 1,5,6,EXTCOLOR;
∀I 7 S;
∀E DEFINITIONS5 G GREEN;
TAUT FREEOF(G GREEN) 8 9;
⊃I 1⊃10;
∀I 11 G;
REPRESENT * AS UNIVERSE;
ATTACH GRID (DE GRID (L)(AND
		 (EQ (LENGTH L) 2)
		 (EQ (LENGTH (CAR L)) 2)
		 (EQ (LENGTH (CADR L)) 2)
		 (COLOR (CAAR L))
		 (COLOR (CADAR L))
		 (COLOR (CAADR L))
		 (COLOR (CADADR L))));
ATTACH COLOR (DE COLOR (X)
	     (MEMQ X (QUOTE (RED GREEN YELLOW BLUE))));
ATTACH RED ↔ RED;
ATTACH GREEN ↔ GREEN;
ATTACH YELLOW ↔ YELLOW;
ATTACH BLUE ↔ BLUE;
comment > we really don't want YELLOW attached to Y >
comment + ATTACH YELLOW ↔ Y; +
EXTENSION COLOR {YELLOW BLUE GREEN RED};
EXTENSION SQUARE {S11 S12 S21 S22};
DECLARE INDCONST MYGRID ε GRID;
ATTACH MYGRID ↔ ((YELLOW YELLOW)(BLUE BLUE));
ATTACH HAS (DE HAS (G C)
		(AND(GRID G)
		    (OR
			 (MEMQ C (CAR G))
			 (MEMQ C (CADR G)))));
ATTACH FREEOF (LAMBDA (G C)(AND (GRID G)(NOT (HAS G C))));
SIMPLIFY ¬YELLOW=BLUE;
SIMPLIFY HAS(MYGRID YELLOW);
SIMPLIFY HAS(MYGRID RED);
SIMPLIFY FREEOF(MYGRID GREEN);
SIMPLIFY ∀C.(HAS(MYGRID C)⊃((C=YELLOW∨C=BLUE)∧¬C=RED));
FUNCTION (DE MAKEPAIR (X Y)(CONS X (CONS Y NIL)));
ATTACH MAKEGRID (LAMBDA (A B C D)
		(MAKEPAIR (MAKEPAIR A B)(MAKEPAIR C D)));
FUNCTION (DE NEXT (S L)
 	(COND ((EQ (CAR L) S)(CADR L))(T (NEXT S (CDR L)))));
ATTACH → (DE → (S)(NEXT S (QUOTE (S11 S12 S22 S21 S11))));
ATTACH S11 ↔ S11;
ATTACH S12 ↔ S12;
ATTACH S21 ↔ S21;
ATTACH S22 ↔ S22;
comment > cancel all steps back to line one with the command >
CANCEL 1;
LABEL THISLINE;
ASSUME PLAID G∧COLOROF(G,S12)=RED;
ASSUME COLOROF(G,S11)=RED;
∀E DEFINITIONS4 G;
LABEL ALLSQ;
TAUT 3:#2 1,3; 
∀E ↑ S12;
∃E ↑ C1 C2;
SIMPLIFY →(→(S12));
SUBSTR ↑ IN ↑↑;
∀E ALLSQ S21;
∃E ↑ CA CB;
SIMPLIFY S11=→(S21);
SUBST ↑ IN ↑↑ OCC 1;
TAUTEQ FALSE THISLINE,2,8:↑;
¬I ↑,THISLINE+1;
⊃I THISLINE⊃↑;
∀I ↑ G←G1;
comment > the show commands >
SHOW AXIOMS;
SHOW AXIOMS DEFINITIONS,EXTCOLOR1;
SHOW PROOF THISLINE,7,↑↑↑:↑;
SHOW AXIOMS DEFINITIONS3,NEXTSQUARE;
SHOW DECLARATIONS INDCONST;
SHOW DECLARATIONS G,MAKEGRID,COLOR,YELLOW,FOOBAZ;
SHOW LABELS 1:12;
SHOW LABELS THISLINE;
SHOW PROOF 9:475 → THIS.PRF[FOL,REF];
Deduce the WFF
		∃X.(P(X)∧Q(X))⊃(∃X.P(X)∧∃X.Q(X))  .
Difficulty = 5
This is example 2-24 in Manna.

Solution:

DECLARE PREDCONST P Q 1;
DECLARE INDVAR X;

ASSUME ∃X.(P(X)∧Q(X));
∃E 1 X;
TAUT ↑:#1 2;
TAUT ↑↑:#2 2;
∃I 3 X;
∃I 4 X;
TAUT 5:∧6: 5 6;
⊃I 1 7;